{\rtf1\ansi\ansicpg1252\cocoartf1138\cocoasubrtf470
{\fonttbl\f0\fswiss\fcharset0 Helvetica;\f1\fnil\fcharset0 Calibri;\f2\froman\fcharset0 TimesNewRomanPSMT;
}
{\colortbl;\red255\green255\blue255;\red217\green11\blue0;}
\paperw11900\paperh16840\margl1440\margr1440\margb1417\margt1417\vieww12500\viewh15100\viewkind1
\deftab720
\pard\pardeftab720\ri0

\f0\b\fs28 \cf2 // The BOLD part is already revised!
\b0\fs24 \cf0 \
\
\pard\pardeftab720\ri0

\b \cf0 ----------------------- REVIEW 1 ---------------------\
PAPER: 21\
TITLE: Invariant Preservation In Iterative Modeling\
AUTHORS: Levi Lucio, Eugene Syriani, Moussa Amrani, Qin Zhang and Hans Vangheluwe\
\
OVERALL RATING: -1 (weak reject)
\b0 \
\

\b The authors present an approach to support iterative modeling. The main idea is\
to guarantee that certain properties, which hold for a version of a model, still \
hold for an evolved version of that model. This paper focuses on behavioral \
models expressed in Algebraic Petri Nets with invariants given in terms of \
temporal logic formulae. The models are defined and checked with the existing \
model-checker AlPiNA. However, instead of checking all invariants after each \
evolution step, the authors define a notion of refinement called 'place \
preserving guard strengthening' by restraining the kinds of allowed iterations, \
under which those properties are preserved by construction. \
The contribution of this paper is twofold. (1) Existing work is assembled in a \
smart way such that iterative modeling with invariant preservation is supported. \
(2) The existing work of [19,20] is extended such that guards may be \
strengthened by adding new guards in conjunction. \
\
While the overall idea and the example presented in this paper are very nice, \
there are some shortcomings in the paper.
\b0 \
\

\b * Requirement R2 seems to be wrongly expressed. In Section 2.1, the requirement \
is described that a user cannot open a more confidential file in read mode than \
in write mode, while in Section 2.4, the property P3 and the natural description \
thereof state that for all opened files of the same user, the read file's access \
class must dominate the write file's access class. This should be the other way \
around.
\b0 \
\

\b * It is not clear, whether the proposed guard strengthening approach only allows \
iterations of a model to be further restricted, or whether the information about \
the kind of iteration is used to tune the model-checker, i.e., only properties \
touched by a transformation which is not a refinement must be checked again.
\b0 \

\b * The last part of Definition 4 should be clarified. Why is N' a strengthening \
of N'' and not the other way around? \
\pard\pardeftab720\ri0

\b0 \cf0 \
\pard\pardeftab720\ri0

\b \cf0 * It is stated in the paper that the precise definitions for Definition 4 and \
the proof for Theorem 1 should be found in [13], which is an extended version of\
the submitted paper. When I downloaded the extended paper to read the details, I\
was a bit disappointed, that instead of the promised details, I found a self \
reference to the extended version of the paper. \
However, I found those details in [19]. I guess that this is a mistake, but \
please be careful when citing related work!\
\pard\pardeftab720\ri0

\b0 \cf0 \
\pard\pardeftab720\ri0

\b \cf0 * The proof for Proposition 1 is hard to follow. The function M_new is not \
defined and it remains unclear why the introduction of M_new satisfies the \
proof. To me the proof seems not to be sound. 
\b0 \
\

\b * Related work focuses only on Petri Nets. However, incremental constraint \
checking for arbitrary Ecore models is also done by, e.g., Egyed et al., which \
seems to be very related.
\b0  \
\

\b * There are many typos, missing words, and grammatical errors throughout the \
paper. Please proofread the paper and improve the writing style.\
For example: \
	- two manual evolution that iteratively: something is missing here
\b0 \
	
\b - an user -> a user, an UNIX-like -> a UNIX-like, ... whether using 'a' \
	\'a0or 'an' depends on the pronunciation
\b0 \
	
\b - guard strenghtening -> guard strengthening
\b0 \
	
\b - the plural form of compound nouns is not built by adding 's' to both\
	\'a0nouns, like transitions guards, but adding 's' to only one of them -> \
	\'a0transition guards\
\pard\pardeftab720\ri0

\b0 \cf0 \
\pard\pardeftab720\ri0

\b \cf0 * The formal part of the paper is hard to read due to lack of accuracy. There \
are some undefined symbols (\\mathcal\{N\}, \\mathbb\{M\}, \\mathcal\{M\}, \
\\mathcal\{M\}_PP, \\mathcal\{M\}_PPGS, M_new) and imprecise explanations. 
\b0 \
\
\pard\pardeftab720\ri0\qj

\f1 \cf0 I think this is too much, when you do not have something else to say, you attack the maths\'85 Everything is properly defined, except that we use a \'93compact\'94 style due to the space limitations. For example, from Def. 1:\
\pard\tx11907\pardeftab720\li425\ri658\sb240\sa240\qj
\cf0 An Algebraic Petri Net  consists of [\'85]. \
\pard\pardeftab720\ri0\qj
\cf0 This defines a mathematical structure 
\f2 ,
\f1  member of a set . Since it is announced at the beginning (\'93An algebraic Petri Net\'94), the reader can easily guess that  is a particular Net and that  is the set of such Petri Nets.\
\
The same stands for all other sets mentioned above.\
\pard\pardeftab720\ri0

\f0 \cf0 \
\pard\pardeftab720\ri0

\b \cf0 For example: [from Proof] (ii) if t is enabled in N but not in N', then a new \
marking M_new \{NOT DEFINED\} is produced for N, and the follower marking \{WHICH \
ONE? M'?\} for t is indeed included \{WHERE? AND WHAT DOES THIS MEAN?\} because it \
already was \{WHAT?\} and the new N-marking contains one new marking.
\b0 \
\

\b To summarize, the overall idea described in the paper is nice and definitely \
worth to be discussed at the ME workshop. Unfortunately, the presentation of the \
paper must be improved to accept the paper.
\b0 \
\
\

\b ----------------------- REVIEW 2 ---------------------\
PAPER: 21\
TITLE: Invariant Preservation In Iterative Modeling\
AUTHORS: Levi Lucio, Eugene Syriani, Moussa Amrani, Qin Zhang and Hans Vangheluwe\
\
OVERALL RATING: 1 (weak accept)\
\
In the given paper an iterative behavioral model evolution concept based on algebraic petri nets is introduced.\
The main feature of the approach is the invariant preservation. The invariants are mapped from requirement properties of the evolving system and are used as conditions in the algebraic petri nets.\
A formalized proof of an invariant preserving evolution of the algebraic petri net is given.\
\
The paper starts with a clear motivation of an iterative modeling approach supported by a formalized set of invariants.\
A running example of a simple file system with some security restrictions is introduced to illustrate their approach.\
A given meta model of the file system example is translated to an algebraic petri net and invariants are used to formalize the behavioral requirements of the system.\
The given model checking tool AlPiNA is used for verifying the algebraic petri net. After this definition of a \
basic model more properties are added by extending the invariants during model evolution. A formalized proof is given that shows that the evolved system is still holding the previous invariants.\
The authors are providing a sufficient list of related work.\
\
Points in favor:\
\
- the topic of invariant preserving model evolution is very relevant\
\
- the authors are using an well described example for illustrating their approach\
\
- the authors formalize their approach by giving a proof\
\
- related work was considered\
\
- the paper is well written\
\
- submission guidelines are fulfilled
\b0 \
\
\
Points against:\
\

\b - the overall process of using the algebraic petri nets for modeling does not become clear, e.g., is there something generated from the petri nets or is it just used for documentation and verification?
\b0 \

\b \
- it is not clear how the consistency between the meta model, given requirements and the resulting petri net is assured
\b0 \
\

\b - there is no discussion about limitations of their approach given
\b0 \
\

\b - using the approach for the given example is very illustrative, but information about what kind of systems are suitable for the given approach would help to understand limitations
\b0 \
\

\b - information about complexity and time consumption during model checking would help to understand the practical use of the approach\
\pard\pardeftab720\ri0

\b0 \cf0 \
\pard\pardeftab720\ri0

\b \cf0 - there is no statement about complexity that comes along with changing requirements in an agile/iterative development processes
\b0 \
\

\b - in the introduction the authors talk about "iterative development for Domain-Specific-Languages", but the paper focuses on petri nets only. The authors mention that DSLs can be transformed into petri nets, but are not going into details.
\b0 \
\

\b - some additional related work could be of interest, e.g., Brauer/Gold/Vogler: "A survey of behaviour and equivalence preserving refinements of petri nets" or Peuk Er: "Invariant property preserving extensions of elementary Petri nets"
\b0 \
\

\b - Typo in Proposition 1: "there is two possibilities" -> "there are two possibilities"
\b0 \
\
\

\b ----------------------- REVIEW 3 ---------------------\
PAPER: 21\
TITLE: Invariant Preservation In Iterative Modeling\
AUTHORS: Levi Lucio, Eugene Syriani, Moussa Amrani, Qin Zhang and Hans Vangheluwe\
\
OVERALL RATING: 1 (weak accept)\
\
Based on the fact that the development of system is more and more iterative, the authors propose a formal approach that requirements satisfied at one iteration remain satisfied in the successive iterations. The approach relies on Algebraic Petri nets and the use of model checker. The approach is illustrated on a File Management System.\
\
Strengths:\
- the paper is well written and well organized.\
- the paper addresses a relevant issue that is well motivated\
- the formal definitions guaranty a certain validity and universality of the proposition while obviously keeping in a certain application context (e.g. use of APN)\
- the example in section 2 and then the illustrations of the definitions in section 3 help the reader to better understand by making concrete the formal definitions. It is a shame that only the two first definitions are illustrated. It would have be great that the other ones are also illustrated. It would have made the paper less dense, more accessible.\
\
Weaknesses:\
- as previously said, the paper is really dense. The authors even used a technical paper to omit some parts. The definitions may be hard to follow for a non specialist reader.\
- the relevant part on the evolution in the example is too rapid, not enough detailed. \
- even if the modeling is iterative, the evolution (as suggested by the authors) does not always correspond to addition. It would have been relevant to have an example where one of the cases mentioned at the beginning of section 3 is satisfied. In other terms, the example is very simplistic perhaps too much.\
\
Questions:\
- evolution (even in case of iterative development) may result from change in the requirements. How is this issue addressed by the authors?\
- is it always possible (and justify) to represent a system with an APN? Is it not a little bit heavy? \
- how the respect of the structural properties is verified after each iteration?\
\
Minor remarks:\
- p1, right column, last sentence: two manual evolution\
- according to me, it is A user 
\b0 \

\b - p2, right column, middle: Here the user levi dominates... The formulation is rather strange since according to the definition the dominates relationship concerns two AccessClass and not a user and a file.
\b0 \

\b - p3, left column, end: the definition of tau is not clear
\b0 \

\b - p3, right column, last sentence: the example 2 is not clear since it is written without eugene and that two lines below, eugene appears.
\b0 \

\b - p4, left column, definition 4: what is the relationship between the various items: OR or AND?
\b0 \
}